| Model: | echoring v.1 (MDP) |
| Parameter(s) | ITERATIONS = 100 |
| Property: | MaxOffline1 (prob-reach) |
java -Xms10240m -Xmx10240m -jar ./root/epmc-standard.jar check --model-input-files echoring.jani --model-input-type jani --property-input-names MaxOffline1 --translate-messages false --value-floating-point-output-native true --graphsolver-iterative-stop-criterion relative --graphsolver-iterative-tolerance 1e-6 --const ITERATIONS=100
| Walltime: | 3.085324764251709s |
| Return code: | 0 |
| Note(s): | The tool result '0' is tagged as incorrect. The reference result is '52504150988881911679596397909897334810442463337338867455399558595210531294562028381304092329458957265562428663685703873991737244215466302098559622143988412917602160114187984683464945325595540353683929308707523274373985663026351878025753854892825464036824627318988744613154308988966388899312417572685940140225453376694398971257874112782293129435261865253155373134329631972167335059791798255746915598672999755177376335845857039300256532807593840648369226080153545357569375050962887423993617460146891841020886333594818635896582520372438266037857587942866627670856390243666083578785397370284467594400445229/50000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000' (approx. 1.0500830197776383e-06) which means a relative error of '1.0' which is larger than the goal precision '0.001'. |
| Relative Error: | 1.0 |
assertions-disabled model-checking analysing-property MaxOffline1 start-building-explorer start-building-initial-states-explorer done-building-initial-states-explorer done-building-explorer build-model-start build-model-done 1 0 iterating iterating-done 1 0 num-states-in-filter 1 "initial" model-checking-done 1 command-check-result-is 0.0 MaxOffline1